es:ES, ff:FIFO, f2f+:F2F+-decls. is_req    E 

latex

Definitions	ES, t  T, x:A. B(x), FIFO, F2F+-decls, is_req  , x:A  B(x), x:AB(x), E, Type,
Lemmas	F2F+-decls wf, FIFO wf, event system wf